Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	active(app(nil,YS))	→ mark(YS)
2:	active(app(cons(X,XS),YS))	→ mark(cons(X,app(XS,YS)))
3:	active(from(X))	→ mark(cons(X,from(s(X))))
4:	active(zWadr(nil,YS))	→ mark(nil)
5:	active(zWadr(XS,nil))	→ mark(nil)
6:	active(zWadr(cons(X,XS),cons(Y,YS)))	→ mark(cons(app(Y,cons(X,nil)),zWadr(XS,YS)))
7:	active(prefix(L))	→ mark(cons(nil,zWadr(L,prefix(L))))
8:	active(app(X1,X2))	→ app(active(X1),X2)
9:	active(app(X1,X2))	→ app(X1,active(X2))
10:	active(cons(X1,X2))	→ cons(active(X1),X2)
11:	active(from(X))	→ from(active(X))
12:	active(s(X))	→ s(active(X))
13:	active(zWadr(X1,X2))	→ zWadr(active(X1),X2)
14:	active(zWadr(X1,X2))	→ zWadr(X1,active(X2))
15:	active(prefix(X))	→ prefix(active(X))
16:	app(mark(X1),X2)	→ mark(app(X1,X2))
17:	app(X1,mark(X2))	→ mark(app(X1,X2))
18:	cons(mark(X1),X2)	→ mark(cons(X1,X2))
19:	from(mark(X))	→ mark(from(X))
20:	s(mark(X))	→ mark(s(X))
21:	zWadr(mark(X1),X2)	→ mark(zWadr(X1,X2))
22:	zWadr(X1,mark(X2))	→ mark(zWadr(X1,X2))
23:	prefix(mark(X))	→ mark(prefix(X))
24:	proper(app(X1,X2))	→ app(proper(X1),proper(X2))
25:	proper(nil)	→ ok(nil)
26:	proper(cons(X1,X2))	→ cons(proper(X1),proper(X2))
27:	proper(from(X))	→ from(proper(X))
28:	proper(s(X))	→ s(proper(X))
29:	proper(zWadr(X1,X2))	→ zWadr(proper(X1),proper(X2))
30:	proper(prefix(X))	→ prefix(proper(X))
31:	app(ok(X1),ok(X2))	→ ok(app(X1,X2))
32:	cons(ok(X1),ok(X2))	→ ok(cons(X1,X2))
33:	from(ok(X))	→ ok(from(X))
34:	s(ok(X))	→ ok(s(X))
35:	zWadr(ok(X1),ok(X2))	→ ok(zWadr(X1,X2))
36:	prefix(ok(X))	→ ok(prefix(X))
37:	top(mark(X))	→ top(proper(X))
38:	top(ok(X))	→ top(active(X))

There are 60 dependency pairs:


39:	ACTIVE(app(cons(X,XS),YS))	→ CONS(X,app(XS,YS))
40:	ACTIVE(app(cons(X,XS),YS))	→ APP(XS,YS)
41:	ACTIVE(from(X))	→ CONS(X,from(s(X)))
42:	ACTIVE(from(X))	→ FROM(s(X))
43:	ACTIVE(from(X))	→ S(X)
44:	ACTIVE(zWadr(cons(X,XS),cons(Y,YS)))	→ CONS(app(Y,cons(X,nil)),zWadr(XS,YS))
45:	ACTIVE(zWadr(cons(X,XS),cons(Y,YS)))	→ APP(Y,cons(X,nil))
46:	ACTIVE(zWadr(cons(X,XS),cons(Y,YS)))	→ CONS(X,nil)
47:	ACTIVE(zWadr(cons(X,XS),cons(Y,YS)))	→ ZWADR(XS,YS)
48:	ACTIVE(prefix(L))	→ CONS(nil,zWadr(L,prefix(L)))
49:	ACTIVE(prefix(L))	→ ZWADR(L,prefix(L))
50:	ACTIVE(app(X1,X2))	→ APP(active(X1),X2)
51:	ACTIVE(app(X1,X2))	→ ACTIVE(X1)
52:	ACTIVE(app(X1,X2))	→ APP(X1,active(X2))
53:	ACTIVE(app(X1,X2))	→ ACTIVE(X2)
54:	ACTIVE(cons(X1,X2))	→ CONS(active(X1),X2)
55:	ACTIVE(cons(X1,X2))	→ ACTIVE(X1)
56:	ACTIVE(from(X))	→ FROM(active(X))
57:	ACTIVE(from(X))	→ ACTIVE(X)
58:	ACTIVE(s(X))	→ S(active(X))
59:	ACTIVE(s(X))	→ ACTIVE(X)
60:	ACTIVE(zWadr(X1,X2))	→ ZWADR(active(X1),X2)
61:	ACTIVE(zWadr(X1,X2))	→ ACTIVE(X1)
62:	ACTIVE(zWadr(X1,X2))	→ ZWADR(X1,active(X2))
63:	ACTIVE(zWadr(X1,X2))	→ ACTIVE(X2)
64:	ACTIVE(prefix(X))	→ PREFIX(active(X))
65:	ACTIVE(prefix(X))	→ ACTIVE(X)
66:	APP(mark(X1),X2)	→ APP(X1,X2)
67:	APP(X1,mark(X2))	→ APP(X1,X2)
68:	CONS(mark(X1),X2)	→ CONS(X1,X2)
69:	FROM(mark(X))	→ FROM(X)
70:	S(mark(X))	→ S(X)
71:	ZWADR(mark(X1),X2)	→ ZWADR(X1,X2)
72:	ZWADR(X1,mark(X2))	→ ZWADR(X1,X2)
73:	PREFIX(mark(X))	→ PREFIX(X)
74:	PROPER(app(X1,X2))	→ APP(proper(X1),proper(X2))
75:	PROPER(app(X1,X2))	→ PROPER(X1)
76:	PROPER(app(X1,X2))	→ PROPER(X2)
77:	PROPER(cons(X1,X2))	→ CONS(proper(X1),proper(X2))
78:	PROPER(cons(X1,X2))	→ PROPER(X1)
79:	PROPER(cons(X1,X2))	→ PROPER(X2)
80:	PROPER(from(X))	→ FROM(proper(X))
81:	PROPER(from(X))	→ PROPER(X)
82:	PROPER(s(X))	→ S(proper(X))
83:	PROPER(s(X))	→ PROPER(X)
84:	PROPER(zWadr(X1,X2))	→ ZWADR(proper(X1),proper(X2))
85:	PROPER(zWadr(X1,X2))	→ PROPER(X1)
86:	PROPER(zWadr(X1,X2))	→ PROPER(X2)
87:	PROPER(prefix(X))	→ PREFIX(proper(X))
88:	PROPER(prefix(X))	→ PROPER(X)
89:	APP(ok(X1),ok(X2))	→ APP(X1,X2)
90:	CONS(ok(X1),ok(X2))	→ CONS(X1,X2)
91:	FROM(ok(X))	→ FROM(X)
92:	S(ok(X))	→ S(X)
93:	ZWADR(ok(X1),ok(X2))	→ ZWADR(X1,X2)
94:	PREFIX(ok(X))	→ PREFIX(X)
95:	TOP(mark(X))	→ TOP(proper(X))
96:	TOP(mark(X))	→ PROPER(X)
97:	TOP(ok(X))	→ TOP(active(X))
98:	TOP(ok(X))	→ ACTIVE(X)

The approximated dependency graph contains 9 SCCs: {66,67,89}, {68,90}, {69,91}, {73,94}, {70,92}, {71,72,93}, {75,76,78,79,81,83,85,86,88}, {51,53,55,57,59,61,63,65} and {95,97}.

Consider the SCC {66,67,89}. There are no usable rules. By taking the AF π with π(APP) = π(mark) = 1 together with the lexicographic path order with empty precedence, the rules in {66,67} are weakly decreasing and rule 89 is strictly decreasing. There is one new SCC.
- Consider the SCC {66,67}. By taking the AF π with π(APP) = 1 together with the lexicographic path order with empty precedence, rule 67 is weakly decreasing and rule 66 is strictly decreasing. There is one new SCC.
  - Consider the SCC {67}. By taking the AF π with π(APP) = 2 together with the lexicographic path order with empty precedence, rule 67 is strictly decreasing.

Consider the SCC {68,90}. There are no usable rules. By taking the AF π with π(CONS) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 68 is weakly decreasing and rule 90 is strictly decreasing. There is one new SCC.
- Consider the SCC {68}. By taking the AF π with π(CONS) = 1 together with the lexicographic path order with empty precedence, rule 68 is strictly decreasing.

Consider the SCC {69,91}. There are no usable rules. By taking the AF π with π(FROM) = π(mark) = 1 together with the lexicographic path order with empty precedence, rule 69 is weakly decreasing and rule 91 is strictly decreasing. There is one new SCC.
- Consider the SCC {69}. By taking the AF π with π(FROM) = 1 together with the lexicographic path order with empty precedence, rule 69 is strictly decreasing.

Consider the SCC {73,94}. There are no usable rules. By taking the AF π with π(mark) = π(PREFIX) = 1 together with the lexicographic path order with empty precedence, rule 73 is weakly decreasing and rule 94 is strictly decreasing. There is one new SCC.
- Consider the SCC {73}. By taking the AF π with π(PREFIX) = 1 together with the lexicographic path order with empty precedence, rule 73 is strictly decreasing.

Consider the SCC {70,92}. There are no usable rules. By taking the AF π with π(mark) = π(S) = 1 together with the lexicographic path order with empty precedence, rule 70 is weakly decreasing and rule 92 is strictly decreasing. There is one new SCC.
- Consider the SCC {70}. By taking the AF π with π(S) = 1 together with the lexicographic path order with empty precedence, rule 70 is strictly decreasing.

Consider the SCC {71,72,93}. There are no usable rules. By taking the AF π with π(mark) = π(ZWADR) = 1 together with the lexicographic path order with empty precedence, the rules in {71,72} are weakly decreasing and rule 93 is strictly decreasing. There is one new SCC.
- Consider the SCC {71,72}. By taking the AF π with π(ZWADR) = 1 together with the lexicographic path order with empty precedence, rule 72 is weakly decreasing and rule 71 is strictly decreasing. There is one new SCC.
  - Consider the SCC {72}. By taking the AF π with π(ZWADR) = 2 together with the lexicographic path order with empty precedence, rule 72 is strictly decreasing.

Consider the SCC {75,76,78,79,81,83,85,86,88}. There are no usable rules. By taking the AF π with π(from) = π(prefix) = π(PROPER) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {81,83,88} are weakly decreasing and the rules in {75,76,78,79,85,86} are strictly decreasing. There is one new SCC.
- Consider the SCC {81,83,88}. By taking the AF π with π(from) = π(prefix) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, the rules in {81,88} are weakly decreasing and rule 83 is strictly decreasing. There is one new SCC.
  - Consider the SCC {81,88}. By taking the AF π with π(from) = π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 81 is weakly decreasing and rule 88 is strictly decreasing. There is one new SCC.
    - Consider the SCC {81}. By taking the AF π with π(PROPER) = 1 together with the lexicographic path order with empty precedence, rule 81 is strictly decreasing.

Consider the SCC {51,53,55,57,59,61,63,65}. There are no usable rules. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = π(prefix) = π(s) = 1 together with the lexicographic path order with empty precedence, the rules in {55,57,59,65} are weakly decreasing and the rules in {51,53,61,63} are strictly decreasing. There is one new SCC.
- Consider the SCC {55,57,59,65}. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = π(prefix) = 1 together with the lexicographic path order with empty precedence, the rules in {55,57,65} are weakly decreasing and rule 59 is strictly decreasing. There is one new SCC.
  - Consider the SCC {55,57,65}. By taking the AF π with π(ACTIVE) = π(cons) = π(from) = 1 together with the lexicographic path order with empty precedence, the rules in {55,57} are weakly decreasing and rule 65 is strictly decreasing. There is one new SCC.
    - Consider the SCC {55,57}. By taking the AF π with π(ACTIVE) = π(cons) = 1 together with the lexicographic path order with empty precedence, rule 55 is weakly decreasing and rule 57 is strictly decreasing. There is one new SCC.
      - Consider the SCC {55}. By taking the AF π with π(ACTIVE) = 1 and π(cons) = [1] together with the lexicographic path order with empty precedence, rule 55 is strictly decreasing.

Consider the SCC {95,97}. The usable rules are {1-36}. By taking the AF π with π(active) = π(cons) = π(ok) = π(proper) = π(s) = π(TOP) = 1 together with the lexicographic path order with precedence from ≻ mark, prefix ≻ mark, prefix ≻ nil and zWadr ≻ app ≻ mark, the rules in {8-15,18,20,24-36,97} are weakly decreasing and the rules in {1-7,16,17,19,21-23,95} are strictly decreasing. There is one new SCC.
- Consider the SCC {97}. The usable rules are {1-23,31-36}. By taking the AF π with π(from) = π(mark) = π(prefix) = π(s) = π(TOP) = π(zWadr) = 1 and π(app) = π(cons) = 2 together with the lexicographic path order with precedence ok ≻ active ≻ nil, the rules in {9,11-13,15-23,31-36} are weakly decreasing and the rules in {1-8,10,14,97} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (425.79 seconds) --- May 3, 2006